ESAxioms(E;T;M;
ESAxioms(loc;kind;val;
ESAxioms(when;after;
ESAxioms(sends;sender;index;
ESAxioms(first;pred;
ESAxioms(causl)
== (e, e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e))
== & (e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e)))
== & (e:E.
== & (first(e)
== & ( loc(pred(e)) = loc(e) & causl(pred(e),e)
== & ( & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e))))
== & (e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))))
== & (Trans e,e':E. causl(e,e'))
== & SWellFounded(causl(e,e'))
== & (e:E.
== & (isrcv(kind(e))
== & ( (sends(lnk(kind(e)),sender(e)))[index(e)] = msg(lnk(kind(e));tag(kind(e));val(e)))
== & (e:E. isrcv(kind(e))  causl(sender(e),e))
== & (e, e':E.
== & (causl(e,e')
== & ( first(e') & causl(e,pred(e'))  e = pred(e')
== & (  isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e'))
== & (e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e))))
== & (e:E, l:IdLnk. loc(e) = source(l)  sends(l,e) = nil)
== & (e, e':E.
== & (isrcv(kind(e))
== & ( isrcv(kind(e'))
== & ( lnk(kind(e)) = lnk(kind(e'))
== & ( (causl(e,e')  causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e')))
== & (e:E, l:IdLnk, n:||sends(l,e)||.
== & (e':E. isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n) 

latex

---

clarification:

ESAxioms{i:l}
ESAxioms(E; T; M; loc; kind; val; when; after; sends; sender; index; first; pred; causl)
== (e:E, e':E. loc(e) = loc(e')  Id  causl(e,e')  e = e'  E  causl(e',e))
== & (e:E. first(e)  (e':E. loc(e') = loc(e)  Id  causl(e',e)))
== & (e:E.
== & (first(e)
== & ( loc(pred(e)) = loc(e)  Id & causl(pred(e),e)
== & ( & (e':E. loc(e') = loc(e)  Id  (causl(pred(e),e') & causl(e',e))))
== & (e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))  T(loc(e),x)))
== & (Trans e,e':E. causl(e,e'))
== & strongwellfounded(E; e,e'.(causl(e,e')))
== & (e:E.
== & (isrcv(kind(e))
== & ( (sends(lnk(kind(e)),sender(e)))[index(e)] = msg(lnk(kind(e));tag(kind(e));val(e))  Msg(M))
== & (e:E. isrcv(kind(e))  causl(sender(e),e))
== & (e:E, e':E.
== & (causl(e,e')
== & ( first(e') & causl(e,pred(e'))  e = pred(e')  E
== & (  isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e')  E)
== & (e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))  Id)
== & (e:E, l:IdLnk. loc(e) = source(l)  Id  sends(l,e) = nil  Msg_sub(l;M) List)
== & (e:E, e':E.
== & (isrcv(kind(e))
== & ( isrcv(kind(e'))
== & ( lnk(kind(e)) = lnk(kind(e'))  IdLnk
== & ( (causl(e,e')
== & ( (
== & ( (causl(sender(e),sender(e'))  sender(e) = sender(e')  E & index(e)<index(e')))
== & (e:E, l:IdLnk, n:{0..||sends(l,e)||}.
== & (e':E.
== & (isrcv(kind(e')) & lnk(kind(e')) = l  IdLnk & sender(e') = e  E & index(e') = n  ) 

latex

Definitions	Trans x,y:T. E(x;y), SWellFounded(R(x;y)), Msg(M), l[i], msg(l;t;v), tag(k), destination(l), A, Id, source(l), type List, Msg_sub(l;M), nil, P  Q, P  Q, P  Q, a<b, x:A. B(x), {i..j}, #$n, ||as||, x:A. B(x), A & B, b, isrcv(k), IdLnk, lnk(k), P & Q, s = t, , f(a)
FDL editor aliases	ESAxioms